Nuprl Lemma : rng_when_when
6,26
postcript
pdf
r
:Rng,
b
,
b'
:
,
p
:|
r
|. (when
b
. when
b'
.
p
) = (when
b
b'
.
p
)
|
r
|
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
|
g
|
,
r
+gp
,
AbGrp
,
Group{i}
,
1of(
t
)
,
when
b
.
p
Lemmas
mon
when
when
,
add
grp
of
rng
wf
b
,
abgrp
wf
,
rng
wf
origin
r:Rng, b, b':
, p:|r|. (when b. when b'. p) = (when b 
b'. p) 
|r| r:Rng, b, b':, p:|r|. (when b. when b'. p) = (when b b'. p) |r| x:A. B(x) T
+gp